\section{Módulo LinkLinkIt}

\begin{Interfaz}
  
	\textbf{se explica con}: \tadNombre{LinkLinkIt}, \tadNombre{Iterador Unidireccional(nodoItlli)}

	\begin{Tupla}[nodoItlli]
		\tupItem{link}{string}
		\tupItem{cat}{string}
		\tupItem{accesosRecientes}{nat}
	\end{Tupla}

	\textbf{géneros}: \TipoVariable{lli}, \TipoVariable{itlli}
	
	\Titulo{Operaciones de LinkLinkIt}

	\InterfazFuncion{Iniciar}{\In{ac}{acat}}{ lli}
	{$\somb{res} \igobs iniciar(\somb{ac}) \land alias(categorias(\somb{res}) \igobs \somb{ac})$}
	[$\Theta(\#categorias(ac))$]
	[Crea un LinkLinkIt]
	
	\InterfazFuncion{NuevoLink}{\Inout{s}{lli}, \In{l}{string}, \In{c}{string}}{}
	[$\somb{s} \igobs s_0 \land \neg(\somb{l} \in links(\somb{s})) \land est\acute{a}?(\somb{c}, categorias(\somb{s}))$]
	{$\somb{s} \igobs nuevoLink(s_0,\somb{l},\somb{c})$}
	[$\Theta(|l| + |c| + altura(categorias(s)))$]
	[Agrega un link al LinkLinkIt]

	\InterfazFuncion{Acceso}{\Inout{s}{lli}, \In{l}{string}, \In{f}{nat}}{}
	[$\somb{s} \igobs s_0 \land \somb{l} \in links(\somb{s}) \land \somb{f} \ge fechaActual(\somb{s})$]
	{$\somb{s} \igobs acceso(s_0,\somb{l},\somb{f})$}
	[$\Theta(|l| + h)$]
	[Accede a un link]

	\InterfazFuncion{CantLinks}{\In{s}{lli}, \In{c}{string}}{nat}
	[$est\acute{a}?(\somb{c},categorias(\somb{s}))$]
	{$\somb{res} \igobs cantLinks(\somb{s},\somb{c})$}
	[$\Theta(|c|)$]
	[Devuelve la cantidad de links de una categoría]

	\Titulo{Operaciones de itlli}

	\InterfazFuncion{CrearIt}{\In{s}{lli}, \In{c}{string}}{itlli}
	[está?($\somb{c}$,categorias($\somb{s}$))]
	{alias($Siguientes(\somb{res}) \igobs ConstruirSecuencia(\somb{s},\somb{c})$)}
	[$\Theta(|c| + n^2)$]
	[Crea el iterador. Llamadas consecutivas con el mismo parámetro (es decir, \\
		un LinkLinkIt que no fue modificado) tienen complejidad $\Theta(|c|)$]

	\InterfazFuncion{HayMas}{\In{it}{itlli}}{bool}
	{$\somb{res} \igobs$~ HayMas?($\somb{it}$)}
	[$\Theta(1)$]
	[Indica si hay más elementos.]

	\InterfazFuncion{Siguiente}{\In{it}{itlli}}{nodoItlli}
	{alias($\somb{res} \igobs$~ Actual(it))}
	[$\Theta(1)$]
	[Devuelve el elemento siguiente.]

	\InterfazFuncion{Avanzar}{\Inout{it}{itlli}}{}
	[$\somb{it} \igobs it_0 \land$~ HayMas?($\somb{it}$)]
	{$\somb{it} \igobs$~ Avanzar($it_0$)}
	[$\Theta(1)$]
	[Avanza al próximo elemento.]


\end{Interfaz}

\begin{Representacion}
	\Titulo{Representación de lli}

	\begin{Estructura}{lli}[estr]
		\begin{Tupla}[estr]
			\tupItem{links}{dicctrie(puntero(nodoLink))}
			\tupItem{cats}{arreglo\_dimensionable de puntero(nodoCat)}
			\tupItem{ac}{acat}
			\tupItem{fechaActual}{nat}
			\tupItem{version}{nat}
		\end{Tupla}

		\begin{Tupla}[nodoLink]
			\tupItem{nombre}{string}
			\tupItem{accesos}{arreglo[3] de accestr}
			\tupItem{fechaRegistro}{nat}
			\tupItem{cat}{string}
		\end{Tupla}

		\begin{Tupla}[nodoCat]
			\tupItem{total}{nat}
			\tupItem{links}{lista(puntero(nodoLink))}
			\tupItem{padre}{puntero(nodoCat)}
			\tupItem{version}{nat}
			\tupItem{fechas}{arreglo[3] de nat}
		\end{Tupla}

		\begin{Tupla}[accestr]
			\tupItem{valido}{bool}
			\tupItem{fecha}{nat}
			\tupItem{accesos}{nat}
		\end{Tupla}
	\end{Estructura}
	
	\Subtitulo{invariante en castellano}

	\begin{enumerate}
		\item Todas los ids de las categorías de $ac$ tienen que estar definidos en $cats$.
		\item	Tienen que haber la misma cantidad de categorías en $cats$ que en $ac$.
		\item Todos los punteros de $links$ tiene que ser válidos ($\neq$ NULL).
		\item Todos los punteros de $cats$ tienen que ser válidos ($\neq$ NULL).
		\item Para todas las categorías en $cats$ el padre tiene que ser un puntero válido a una categoría dentro
				$cats$, a menos que sea la raíz.
		\item Para todas las categorías en $ac$ el id del padre de la categoría tiene que ser el mismo que el
				que tiene el puntero $padre$ dentro de $cats$, a menos que sea la raíz.
		\item Las categorías de los links tienen que ser válidas (tienen que pertencer al árbol de categorías).
		\item Los links de cada categoría tiene que pertenecer al diccionario de links.
		\item Para cada link, éste tiene que aparecer en los links de la categoría a la que pertenece.
		\item Para cada link dentro del campo $links$ de cada categoría en $cats$, éste tiene que tener como
				$cat$ a dicha categoría o a alguna de sus hijas.
		\item Para cada categoría los links de todas las categorías hijas tienen que estar en los links de la
				categoría.
		\item La lista de links dentro de cada categoría en $cats$ no tiene repetidos.
		\item Cada link en $links$ debe tener como campo $link$ a la clave con la que está definido dentro del
				diccionario $links$.
		\item Para cada categoría en $cats$ el campo $total$ es igual a la cantidad de links en $links$.
		\item El campo $version$ tiene que ser mayor o igual a los campos $version$ de todas las categorías en
				$cats$.
		\item Si el campo $version$ de una categoría en $cats$ es igual al campo $version$ de $estr$ entonces
				la lista $links$ está ordenada por accesos recientes.
		\item El campo $fecha$ de cada uno de los accesos válidos (con $valido$ = true) de cada link en $links$ tiene que
				ser menor a la menor de las fechas de la categoría a la que pertenece o ser alguna de esas fechas sí y sólo sí la versión
				de la categoría es igual a la versión de $e$.
		\item El campo $fecha$ de cada uno de los accesos válidos (con $valido$ = true) de cada link en $links$ tiene que ser mayor
				o igual a la fecha de registro del link.
		\item Para cada link la fecha de registro debe ser menor o igual a la fecha actual del sistema.
		\item La fecha actual es igual a la fecha del más reciente de todos los accesos.
		%\item El campo $fecha$ de cada uno de los $accesos$ válidos (campo $valido$ = true) de cada link $links$ tiene que ser menor o igual a
		%		la mayor de las fechas en el campo $fechas$ de su categoría y de todas sus categorías padres.
				% NOTE: Hay que pedir algo más fuerte, como que no se puede dar que fechas sea [28,17,21]
				% y que accesos tenga como fechas [27, 22, 13]. Pero me da paja pensarlo.
	\end{enumerate}
	
	~
	
	\Subtitulo{invariante}
	
	~
	
	\Rep[$\somb{estr}$][e]{
		(\paratodo{categoría}{c})(($c$ $\in$ categorías($e$.ac)) \impluego definido?(id($c$, $e$.ac), $e$.cats))) \\
		$\land$ (\#(categorías($e$.ac)) \igobs tam($e$.cats)) \\
		$\land$ (\paratodo{nat}{n})(definido?($n$, $e$.cats) \impluego $\neg$($e$.cats[$n$] \igobs NULL)) \\
		$\land$ (\paratodo{link}{l})(def?($l$, $e$.links) \impluego $\neg$(obtener($l$, $e$.links) \igobs NULL)) \\
		\yluego (\paratodo{nat}{n})(definido?($n$, $e$.cats) \impluego (id(raiz($e$.ac)) \igobs $n$ \oluego (\existe{nat}{n'})((definido?($n'$, $e$.cats) \yluego ($e$.cats[$n$]\DRef padre \igobs $e$.cats[$n'$]))))) \\
		\yluego (\paratodo{categoría}{c})(($c$ $\in$ categorías($e$.ac)) \impluego ((id($c$, $e$.ac) = id(raiz($e$.ac))) \oluego id(padre($c$, $e$.ac), $e$.ac) = ObtenerÍndice($e$.cats[id($c$, $e$.ac)]\DRef padre, $e$.cats))) \\
		\yluego (\paratodo{link}{l})(def?($l$, $e$.links) \impluego (obtener($l$, $e$.links)\DRef cat $\in$ categorías($e$.ac))) \\
		\yluego (\paratodo{nat}{n})(definido?($n$, $e$.cats) \impluego (\paratodo{puntero(nodoLink)}{l})(está?($l$, $e$.cats[$n$]\DRef links) \impluego ExisteElLink($l$, $e$.links))) \\
		\yluego (\paratodo{nat}{n})(definido?($n$, $e$.cats) \impluego (\paratodo{puntero(nodoLink)}{l})((está?($l$, $e$.cats[$n$]\DRef links) \impluego ($l$\DRef cat \igobs CategoríaConId($n$, $e$.ac) $\lor$ esSubCategoría($e$.ac, CategoríaConId($n$, $e$.ac), $l$\DRef cat)))) \\
		\yluego (\paratodo{nat}{n})(definido?($n$, $e$.cats) \impluego (\paratodo{categoría}{c})(($c$ $\in$ categorías($e$.ac) \yluego $\;$ esSubCategoría($e$.ac, CategoríaConId($n$, $e$.ac), $c$)) \impluego ((\paratodo{link}{l})(está?($l$, $e$.cats[id($c$, $e$.ac)]\DRef links) $\implies$ está?($l$, $e$.cats[$n$]\DRef links)))))) \\
		\yluego (\paratodo{link}{l})(def?($l$, $e$.links) \impluego (está?(obtener($l$, $e$.links), $e$.cats[id(obtener($l$, $e$.links)\DRef cat, $e$.ac)]\DRef links))) \\
		\yluego (\paratodo{nat}{n})(definido?($n$, $e$.cats) \impluego (Únicos($e$.cats[$n$]\DRef links))) \\
		\yluego (ArmarConjunto($e$.cats[id(raíz($e$.ac))]\DRef hijos) \igobs claves($e$.links)) \\
		\yluego (\paratodo{link}{l})(def?($l$, $e$.links) \impluego (obtener($l$, $e$.links)\DRef link \igobs $l$) \\
		\yluego (\paratodo{nat}{n})(definido?($n$, $e$.cats) \impluego $e$.cats[$n$]\DRef total \igobs long($e$.cats[$n$]\DRef hijos)) \\
		\yluego (\paratodo{nat}{n})(definido?($n$, $e$.cats) \impluego $e$.cats[$n$]\DRef version $\leq$ $e$.version) \\
		\yluego (\paratodo{nat}{n})((definido?($n$, $e$.cats) \yluego $e$.cats[$n$]\DRef version \igobs $e$.version) \impluego OrdenadaPorAccesos($e$.cats[$n$]\DRef hijos, $e$.cats[$n$])) \\
		\yluego (\paratodo{link}{l})((def?($l$, $e$.links) \yluego ($e$.cats[id(obtener($l$, $e$.links)\DRef cat, $e$.ac)]\DRef version \igobs $e$.version) \impluego AccesosVálidos(obtener($l$, $e$.links)\DRef accesos, $e$.cats[id(obtener($l$, $e$.links)\DRef cat, $e$.ac)])) \igobs $l$) \\
		\yluego (\paratodo{link}{l})(def?($l$, $e$.links) \impluego FechasAccesosMayoresAlRegistro(obtener($l$, $e$.links)\DRef accesos, obtener($l$, $e$.links)))) \\
		\yluego (\paratodo{link}{l})(def?($l$, $e$.links) \impluego (obtener($l$, $e$.links)\DRef fechaRegistro $\leq$ $e$.fechaActual)) \\
		$\land$ $e$.fechaActual \igobs BuscarFechaActual($e$.links) \\
	}
	
	\vspace{15pt}
	~
	
	\tadOperacion{ObtenerÍndice}{puntero(nodoCat)/p, arreglo\_dimensionable$\;$de$\;$puntero(nodoCat)/cats}{nat}{(\existe{nat}{n})(defindo?($n$, $cats$) \yluego ($p$ \igobs $cats$[$n$]))}
	\tadAxioma{ObtenerÍndice($p$, $cats$)}{ObtenerÍndiceAux($p$, $cats$, tam($cats$) $-$ 1)}
	
	~
	
	\tadOperacion{ObtenerÍndiceAux}{puntero(nodoCat)/p, arreglo\_dimensionable$\;$de$\;$puntero(nodoCat)/cats, nat/i}{nat}{(\existe{nat}{n})(defindo?($n$, $cats$) \yluego ($p$ \igobs $cats$[$n$])) $\land$ $i <$ tam($cats$)}
	\tadAxioma{ObtenerÍndiceAux($p$, $cats$, $i$)}{\IF $cats$[$i$] = $p$ THEN $i$ ELSE ObtenerÍndiceAux($p$, $cats$, $i$ $-$ 1) FI}
	
	~
	
	\tadOperacion{Únicos}{secu($\alpha$))}{bool}{}
	\tadAxioma{Unicos($s$)}{$\neg$(está?(prim($s$),fin($s$))) \yluego Unicos(fin($s$))}
	
	~
	
	\tadOperacion{OrdenadaPorAccesos}{secu(puntero(nodoLink)), puntero(nodoCat)}{bool}{}
	\tadAxioma{OrdenadaPorAccesos($links$, $c$)}{
		\IF long($links$) $<$ 2 THEN true ELSE SumarAccesos(prim($links$), $c$) $>$ SumarAccesos(prim(fin($links$)), $c$) $\land$ OrdenadaPorAccesos(fin($links$), $c$) FI
	}
	
	\vspace{15pt}
	~
	
	\tadOperacion{SumarAccesos}{puntero(nodoLink), puntero(nodoCat)}{nat}{}
	\tadAxioma{SumarAccesos($l$, $c$)}{
		\IF $l$\DRef accesos[0].valido \igobs true $\land$ Está($l$\DRef accesos[0].fecha, $c$\DRef fechas) THEN $l$\DRef accesos[0].accesos ELSE 0 FI $+$
		\IF $l$\DRef accesos[1].valido \igobs true $\land$ Está($l$\DRef accesos[1].fecha, $c$\DRef fechas) THEN $l$\DRef accesos[1].accesos ELSE 0 FI $+$
		\IF $l$\DRef accesos[2].valido \igobs true $\land$ Está($l$\DRef accesos[2].fecha, $c$\DRef fechas) THEN $l$\DRef accesos[2].accesos ELSE 0 FI
	}
	
	\vspace{15pt}
	~
	
	\tadOperacion{Está}{$\alpha$, arreglo\_dimensionable$\;$de$\;\alpha$}{bool}{}
	\tadAxioma{Está($e$, $a$)}{EstáAux($e$, $a$, 0)}
	
	~
	
	\tadOperacion{EstáAux}{$\alpha$, arreglo\_dimensionable$\;$de$\;\alpha$, nat}{bool}{}
	\tadAxioma{EstáAux($e$, $a$, $n$)}{$\neg$($n$ \igobs tam($a$)) \yluego ($a$[$n$] \igobs $e$ $\lor$ Está($e$, $a$, $n$ + 1))}
	
	~
	
	\tadOperacion{AccesosVálidos}{arreglo\_dimensionable$\;$de$\;$accestr, puntero(nodoCat)}{bool}{}
	\tadAxioma{AccesosVálidos($a$, $l$, $c$)}{
		($\neg$($a$[0].válido) \oluego ($a$[0].fecha $<$ Menor($c$\DRef fechas) $\lor$ Está($a$[0].fecha, $c$\DRef fechas))) \\ 
		$\land$ ($\neg$($a$[1].válido) \oluego ($a$[1].fecha $<$ Menor($c$\DRef fechas) $\lor$ Está($a$[1].fecha, $c$\DRef fechas))) \\
		$\land$ ($\neg$($a$[2].válido) \oluego ($a$[2].fecha $<$ Menor($c$\DRef fechas) $\lor$ Está($a$[2].fecha, $c$\DRef fechas)))
	}
	
	\vspace{15pt}
	~
	
	\tadOperacion{FechasAccesosMayoresAlRegistro}{arreglo\_dimensionable$\;$de$\;$accestr, puntero(nodoLink)}{bool}{}
	\tadAxioma{FechasAccesosMayoresAlRegistro($a$, $l$)}{
		($\neg$($a$[0].válido) \oluego ($a$[0].fecha $\geq$ $l$.fechaRegistro)) \\ 
		$\land$ ($\neg$($a$[1].válido) \oluego ($a$[1].fecha $\geq$ $l$.fechaRegistro)) \\
		$\land$ ($\neg$($a$[2].válido) \oluego ($a$[2].fecha $\geq$ $l$.fechaRegistro))
	}
	
	~
	
	\tadOperacion{Menor}{arreglo\_dimensionable$\;$de$\;$nat/a}{bool}{tam($a$) $>$ 0}
	\tadAxioma{Menor($a$)}{MenorAux($e$, $a$, 0)}
	
	~
	
	\tadOperacion{MenorAux}{arreglo\_dimensionable$\;$de$\;$nat, nat}{bool}{tam($a$) $>$ 0 $\land$ $n$ < tam($n$)}
	\tadAxioma{MenorAux($a$, $n$)}{
		\IF $n$ = (tam($a$) $-$ 1) THEN $a$[$n$] ELSE min($a$[$n$], MenorAux($a$, $n$ $+$ 1)) FI
	}
	
	~
	
	\tadOperacion{ExisteElLink}{puntero(nodoLink), dicc(nodoLink)}{bool}{}
	\tadAxioma{ExisteElLink($p$, $d$)}{ExisteElLinkAux($p$, $d$, claves($d$))}
	
	~
	
	\tadOperacion{ExisteElLinkAux}{puntero(nodoLink)/p, dicc(nodoLink)/d, conj(link)/c}{bool}{(\paratodo{link}{l})($l$ $\in$ c $\implies$ def($l$, $d$))}
	\tadAxioma{ExisteElLinkAux($p$, $d$, $c$)}{
		\IF $\emptyset$?($c$) THEN false ELSE obtener(dameUno($c$), $d$) \igobs $p$ $\lor$ ExisteElLinkAux($p$, $d$, sinUno($c$)) FI
	}
	
	\vspace{15pt}
	~
	
	\tadOperacion{BuscarFechaActual}{dicc(puntero(nodoLink))}{nat}{}
	\tadAxioma{BuscarFechaActual($d$)}{
		\IF $\emptyset$?(FechasDeAccesosVálidos($d$)) THEN 0 ELSE Mayor(FechasDeAccesosVálidos($d$)) FI
	}
	
	~
	
	\tadOperacion{FechasDeAccesosVálidos}{dicc(puntero(nodoLink))}{conj(nat)}{}
	\tadAxioma{FechasDeAccesosVálidos($d$)}{FechasDeAccesosVálidosAux($d$, claves($d$))}
	
	~
	
	\tadOperacion{FechasDeAccesosVálidosAux}{dicc(puntero(nodoLink))/d, conj(link)/cs}{conj(nat)}{(\paratodo{link}{l})(($l$ $\in$ $cs$) $\implies$ def?($l$, $d$))}
	\tadAxioma{FechasDeAccesosVálidosAux($d$, $cs$)}{
		\IF $\emptyset$?($cs$) THEN $\emptyset$ ELSE {\IF obtener(dameUno($cs$), $d$)\DRef valido THEN Ag(dameUno($cs$), FechasDeAccesosVálidosAux($d$, sinUno($cs$))) ELSE FechasDeAccesosVálidosAux($d$, sinUno($cs$)) FI} FI
	}
	
	~
	
	\tadOperacion{Mayor}{conj(nat)}{nat}{\#($c$) > 0}
	\tadAxioma{Mayor($c$)}{
		\IF \#($c$) $<$ 2 THEN dameUno($c$) ELSE max(dameUno(cs), Mayor(sinUno($cs$))) FI
	}
	
	~
	
	\tadOperacion{CategoríaConId}{nat/id, acat/ac}{categoría}{(\existe{categoría}{c})(($c$ $\in$ categorías($ac$)) \yluego (id($c$, $ac$) \igobs id))}
	\tadAxioma{CategoríaConId($id$, $ac$)}{CategoríaConIdAux($id$, $ac$, categorías($ac$))}
	
	~
	
	\tadOperacion{CategoríaConIdAux}{nat/id, acat/ac, conj(categoría)/cats}{categoría}{(\paratodo{categoría}{c})($c$ $\in$ $cats$ \impluego $c$ $\in$ categorías($ac$)) $\land$ (\existe{categoría}{c})(($c$ $\in$ categorías($ac$) \yluego (id($c$, $ac$) \igobs id))}
	\tadAxioma{CategoríaConIdAux($id$, $ac$, $cats$)}{
		\IF id(dameUno($cats$), $ac$) \igobs $id$ THEN dameUno($cats$) ELSE CategoríaConIdAux($id$, $ac$, sinUno($cats$)) FI
	}
	
% 	\tadOperacion{LinkVálidoEnCat}{puntero(nodoLink)/l, puntero(nodoCat)/c, categoría/cat, acat/ac}{bool}{}
% 	\tadAxioma{LinkVálidoEnCat($l$, $c$)}{
% 		\IF $\emptyset$?($c$) THEN false ELSE obtener(dameUno($c$), $d$) \igobs $p$ $\lor$ ExisteElLinkAux($p$, $d$, sinUno($c$)) FI
% 	}
	
	
	\Subtitulo{función de abstracción}
	
	~
	
	\Abs[$\somb{estr}$]{$\somb{lli}$}[e]{lli}{
		(categorías($lli$) \igobs $e$.ac) $\land$ (links($lli$) \igobs claves($e$.links))
		$\land$ fechaActual($lli$) = $e$.fechaActual \yluego
		(\paratodo{link}{l})(($l$ $\in$ links($lli$)) \impluego ( (categoriaLink($lli$,$l$) \igobs obtener($l$, $e$.links)\DRef cat) \\
		$\land$ (fechaUltimoAcceso($lli$, $l$) \igobs FechaUltimoAcceso(obtener($l$, $e$.links))) ) \yluego \\
		(\paratodo{link}{l})(\paratodo{fecha}{f}) ($l \in$~ links($lli$) \yluego esReciente?($lli$,$l$,$f$)) $\implies$ \\
		accesosRecientesDia($lli$,$l$,$f$) \igobs ObtenerAccesosDelDia(obtener($l$, $e$.links),$f$)
	}

	~

	\tadOperacion{ObtenerAccesosDelDia}{puntero(nodoLink)/nl,fecha/f}{nat}{$\neg$(nl = NULL)}
	\tadAxioma{ObtenerAccesosDelDia($nl$,$f$)}{
		\IF nl\DRef accesos[0].valido \yluego accesos[0].fecha = f THEN accesos[0].accesos ELSE{
			\IF nl\DRef accesos[1].valido \yluego accesos[1].fecha = f THEN accesos[1].accesos ELSE{
				\IF nl\DRef accesos[2].valido \yluego accesos[2].fecha =f THEN accesos[2].accesos ELSE 0 FI
			} FI
		} FI
	}
	
	~
	
	\tadOperacion{FechaUltimoAcceso}{puntero(nodoLink)/nl}{nat}{$\neg$($nl$ = NULL)}
	\tadAxioma{FechaUltimoAcceso($nl$)}{
		máx( {\IF (*nl).accesos[0].valido THEN (*nl).accesos[0].fecha ELSE (*nl).fechaRegistro FI},
			máx( {\IF (*nl).accesos[1].valido THEN (*nl).accesos[1].fecha ELSE (*nl).fechaRegistro FI},
				{\IF (*nl).accesos[2].valido THEN (*nl).accesos[2].fecha ELSE (*nl).fechaRegistro FI} ) )
	}
	
	~
	
	\Titulo{Representación del iterador}
	
	\begin{Estructura}{itlli}[estrItlli]
		\begin{Tupla}
			\tupItem{lista}{itLista(puntero(nodoLink))}
			\tupItem{fechas}{arreglo[3] de nat}
		\end{Tupla}
	\end{Estructura}

	~

	\Rep[$\somb{estrItlli}$][e]{$\neg$está?(NULL,SecuSuby($e$.lista)) \yluego ((\paratodo{nat}{n})($n < 3$) $\implies$ definido?($e$.fechas,$n$)) $\land$ EstáOrdenado(SecuSuby($e$.lista), $e$.fechas)}

	~

	\tadOperacion{EstáOrdenado}{secu(puntero(nodoLink))/links, ad(nat)/fechas}{bool}{$\neg$ está?(NULL,$links$) $\land$ ((\paratodo{nat}{n}) ($n < 3$) $\implies$ definido?($fechas$,$n$))}
	\tadAxioma{EstáOrdenado($links$, $fechas$)}{
		\IF long($links$) $<$ 2 THEN \textbf{true} ELSE SumarAccesosArreglo(prim($links$), $fechas$) $>$ SumarAccesosArreglo(prim(fin($links$)), $fechas$) $\land$ EstáOrdenado(fin($links$), $fechas$) FI
	}
	
	~
	

	\Abs[$\somb{estrItlli}$]{itUni(nodoItlli)}[e]{it}{
		Siguientes($it$) $\igobs$ ConstruirSecu($e$.fechas, Siguientes($e$.lista))
	}

	~

	\tadOperacion{ConstruirSecu}{ad(nat)/fechas, secu(puntero(nodoLink))/s}{secu(nodoItlli)}{$\neg$está?(NULL,$s$) $\land$ ((\paratodo{nat}{n})($n < 3$) $\implies$ definido?($fechas$,$n$))}
	\tadAxioma{ConstruirSecu($fechas$,$s$)}{
		\IF vacía?($s$) THEN $<>$ ELSE {
			$\langle$(*prim($s$)).nombre, (*prim($s$)).cat, SumarAccesosArreglo(prim($s$),$fechas$)$\rangle$
			\puntito ConstruirSecu($fechas$,fin($s$))
		}
		FI
	}

	~

	\tadOperacion{SumarAccesosArreglo}{puntero(nodoLink)/l, ad(nat)/fechas}{nat}{$\neg$(l = NULL) $\land$ ((\paratodo{nat}{n})($n < 3$) $\implies$ definido?($fechas$,$n$))}
	\tadAxioma{SumarAccesosArreglo($l$, $fechas$)}{
		\IF $l$\DRef accesos[0].valido $\land$ Está($l$\DRef accesos[0].fecha, $fechas$) THEN $l$\DRef accesos[0].accesos ELSE 0 FI $+$
		\IF $l$\DRef accesos[1].valido $\land$ Está($l$\DRef accesos[1].fecha, $fechas$) THEN $l$\DRef accesos[1].accesos ELSE 0 FI $+$
		\IF $l$\DRef accesos[2].valido $\land$ Está($l$\DRef accesos[2].fecha, $fechas$) THEN $l$\DRef accesos[2].accesos ELSE 0 FI
	}

	~

	\tadOperacion{ConstruirSecuencia}{lli/s, categoría/c}{secu(nodoItlli)}{está?(c,categorías(s))}
	\tadAxioma{ConstruirSecuencia($s$,$c$)}{Redefinir(linksOrdenadosPorAccesos(s,c))}

	~
	
	\tadOperacion{Redefinir}{secu(link)}{secu(nodoItlli)}{}
	\tadAxioma{Redefinir($s$)}{\IF $\neg$vacía?($s$) THEN $\langle$prim($s$), categoriaLink($s$,prim($s$)), accesosRecientes($s$,categoriaLink($s$,prim($s$)),prim($s$))$\rangle$ \puntito Redefinir(fin($s$)) ELSE $<>$ FI}

\end{Representacion}

\begin{Algoritmos}

\Implementacion{iIniciar}{\In{ac}{acat}}{ lli}
\begin{algorithmic}
	\State var it : itAcat

	\State \res.ac \asignar ac
	\State \res.version \asignar 1
	\State \res.cats \asignar CrearArreglo( CantCategorias( ac ) + 1 ) % Indizado de 1..n (id raiz = 1).
	\State \res.links \asignar Vacío()
	\State \res.fechaActual \asignar 0
	\State \res.cats[1] \asignar CrearNodoCat() % La raíz

	\State it \asignar CrearItHijosRaiz(ac)
	\While{HayMas(it)}
		\State AgregarCategoria( Siguiente(it) )
		\State AgregarHijos( it )
		\State Avanzar(it)
	\EndWhile
\end{algorithmic}

~

\Implementacion{AgregarCategoria}{\In{n}{nodoItAc}}{}
\begin{algorithmic}
	\State var nc : puntero(nodoCat) \asignar CrearNodoCat()
	\If{n.tienePadre}
		\State (*nc).padre = s.cats[n.padreId]
	\EndIf
	\State s.cats[n.id] \asignar nc
\end{algorithmic}

~

\Implementacion{AgregarHijos}{\In{it}{itAcat}}{}
\begin{algorithmic}
	\State var hijos : itAcat \asignar CrearItHijosIt(it)
	\While{HayMas(hijos)}
		\State AgregarCategoria( Siguiente(hijos) )
		\State AgregarHijos( hijos )
		\State Avanzar( hijos )
	\EndWhile
\end{algorithmic}

~

\Implementacion{NuevoLink}{\Inout{s}{lli}, \In{l}{string}, \In{c}{string}}{}
\begin{algorithmic}
	\State var nl : puntero(nodoLink)
	\State var nc : puntero(nodoCat)
	\State nl \asignar CrearNodoLink(l,c)
	\State (*nl).fechaRegistro \asignar s.fechaActual
	\State s.version \asignar s.version + 1
	\State Definir( s.links, l, nl )
	\State nc \asignar s.cats[Id(s.ac,c)]
	\While{$\neg$(nc = NULL)}
		\State (*nc).total \asignar (*nc).total + 1
		\State AgregarAtras( (*nc).links, nl )
		\State nc \asignar (*nc).padre
	\EndWhile
\end{algorithmic}

~

\Implementacion{CrearNodoCat}{}{puntero(nodoCat)}
\begin{algorithmic}
	\State var nc : nodoCat
	\State nc.total \asignar 0
	\State nc.links \asignar Vacía()
	\State nc.padre \asignar NULL
	\State nc.version \asignar 0
	\State nc.fechas[0] \asignar 0
	\State nc.fechas[1] \asignar 0
	\State nc.fechas[2] \asignar 0
	\State \res \asignar \&nc
\end{algorithmic}

~

\Implementacion{CrearNodoLink}{\In{l}{string},\In{c}{string}}{puntero(nodoLink)}
\begin{algorithmic}
	\State var nl : nodoLink
	\State var n : nat
	\State nl.nombre \asignar l
	\State nl.cat \asignar c
	\State nl.fechaRegistro \asignar 0
	\For{n \asignar 0 \textbf{to} 2}
		\State nl.accesos[n].fecha \asignar 0
		\State nl.accesos[n].accesos \asignar 0
		\State nl.accesos[n].valido \asignar false
	\EndFor
	\State \res \asignar \&nl
\end{algorithmic}

~

\Implementacion{Acceso}{\Inout{s}{lli}, \In{l}{string}, \In{f}{nat}}{}
\begin{algorithmic}
	\State var idx : nat
	\State var nl : puntero(nodoLink) \asignar Obtener( s.links, l )
	
	\State s.version \asignar s.version + 1
	\State s.fechaActual \asignar f

	\State idx \asignar SeleccionarFechaAModificar( nl, f )
	\If{(*nl).accesos[idx].fecha = f}
		\State (*nl).accesos[idx].accesos \asignar (*nl).accesos[idx].accesos + 1
	\Else
		\State (*nl).accesos[idx].fecha \asignar f
		\State (*nl).accesos[idx].accesos \asignar 1
	\EndIf
	\State (*nl).accesos[idx].valido \asignar true
\end{algorithmic}

~

%NOTE: precondición: fecha > fechaactual(s)
\Implementacion{SeleccionarFechaAModificar}{\In{nl}{puntero(nodoLink)}, \In{f}{nat}}{nat}
\begin{algorithmic}
	\State var n, idx : nat
	\State idx \asignar 3

	\For{n \asignar 0 \textbf{to} 2}
		\If{(*nl).accesos[n].valido $\land$ (*nl).accesos[n].fecha = f}%NOTE: El Rep tiene que decir que no puede haber dos campos válidos con la misma fecha. --eze
			\State idx \asignar n
		\EndIf
	\EndFor

	\If{idx > 2}
		\For{n \asignar 0 \textbf{to} 2}
			\If{$\neg$((*nl).accesos[n].valido)}
				\State idx \asignar n
				\State n \asignar 3
			\ElsIf{idx > 2}
				\State idx \asignar n
			\ElsIf{(*nl).accesos[n].fecha < (*nl).accesos[idx].fecha}
				\State idx \asignar n
			\EndIf
		\EndFor
	\EndIf

	\State \res \asignar idx
\end{algorithmic}

~

\Implementacion{CantLinks}{\In{s}{lli}, \In{c}{string}}{nat}
\begin{algorithmic}
	\State var nc : puntero(nodoCat) \asignar s.cats[Id(s.ac,c)]
	\State \res \asignar (*nc).total
\end{algorithmic}

\Titulo{Algoritmos del Iterador}

~

\Implementacion{CrearIt}{\In{s}{lli}, \In{c}{string}}{estrItlli}
\begin{algorithmic}
	\State nc : puntero(nodoCat) \asignar s.cats[Id(s.ac,c)]
	\If{$\neg$((*nc).version = s.version)}
		\State (*nc).fechas \asignar CalcularFechas((*nc).links)
		\State Sort( (*nc).links, (*nc).fechas )
		\State (*nc).version \asignar s.version
	\EndIf
	\State \res.fechas \asignar (*nc).fechas
	\State \res.lista \asignar CrearIt((*nc).links)
\end{algorithmic}

~

\Implementacion{HayMas}{\In{it}{estrItlli}}{bool}
\begin{algorithmic}
	\State \res \asignar HaySiguiente(it.lista)
\end{algorithmic}

~

\Implementacion{Siguiente}{\In{it}{estrItlli}}{nodoItlli}
\begin{algorithmic}
	\State var n : nodoItlli
	\State var nl : puntero(nodoLink) \asignar Siguiente(it.lista)
	\State n.link \asignar (*nl).nombre
	\State n.cat \asignar (*nl).cat
	\State n.accesosRecientes \asignar CalcularAccesosRecientes((*nl).accesos, it.fechas)
	\State \res \asignar \&n
\end{algorithmic}

~

\Implementacion{Avanzar}{\Inout{it}{estrItlli}}{}
\begin{algorithmic}
	\State Avanzar(it.lista)
\end{algorithmic}

~

\Implementacion{CalcularFechas}{\In{links}{lista(puntero(nodoLink))}}{arreglo[3] de nat}
\begin{algorithmic}
	\State var it : itLista(puntero(nodoLink))
	\State var p : puntero(nodoLink)

	\State \res[0] \asignar 0
	\State \res[1] \asignar 0
	\State \res[2] \asignar 0

	\State it \asignar CrearIt(links)
	\While{HaySiguiente(it)}
		\State p \asignar Siguiente(it)
		\State AgregarFechas(\res,(*p).accesos)
		\State Avanzar(it)
	\EndWhile
\end{algorithmic}

~

\Implementacion{AgregarFechas}{\Inout{arr}{arreglo[3] de nat}, \In{fechas}{arreglo[3] de accestr}}{}
\begin{algorithmic}
	\State var i : nat
	\For{i \asignar 0 \textbf{to} 2}
		\If{fechas[i].valido}
			\State AgregarFechaSiVa(arr,fechas[i].fecha)
		\EndIf
	\EndFor
\end{algorithmic}

~

\Implementacion{AgregarFechaSiVa}{\Inout{arr}{arreglo[3] de nat}, \In{f}{nat}}{}
\begin{algorithmic}
	\State var idx : nat
	\If{VaLaFecha(arr,f)}
		\State idx \asignar 0
		\If{arr[idx] $>$ arr[1]}
			\State idx \asignar 1
		\EndIf
		\If{arr[idx] $>$ arr[2]}
			\State idx \asignar 2
		\EndIf
	\EndIf
	\State arr[idx] \asignar f
\end{algorithmic}

~

\Implementacion{VaLafecha}{\In{arr}{arreglo[3] de nat}, \In{f}{nat}}{bool}
\begin{algorithmic}
	\State var i : nat
	\State \res \asignar false
	\For{i \asignar 0 \textbf{to} 2}
		\If{arr[i] $<$ f}
			\State \res \asignar true
		\ElsIf{arr[i] $=$ f}
			\State \res \asignar false
			\State i \asignar 3
		\EndIf
	\EndFor
\end{algorithmic}

~

\Implementacion{CalcularAccesosRecientes}{\In{fl}{arreglo[3] de accestr}, \In{fc}{arreglo[3] de nat}}{nat}
\begin{algorithmic}
	\State var i : nat
	\State \res \asignar 0
	\For{i \asignar 0 \textbf{to} 2}
		\If{fl[i].valido $\land$ (fl[i].fecha = fc[0] $\lor$ fl[i].fecha = fc[1] $\lor$ fl[i].fecha = fc[2])}
			\State \res \asignar \res + fl[i].accesos
		\EndIf
	\EndFor
\end{algorithmic}

~

Sort implementa Bubble Sort, aunque se podría implementar perfectamente Merge Sort y obtener
una complejidad $O(n \cdot \log n)$ (http://www.chiark.greenend.org.uk/{\textasciitilde{}}sgtatham/algorithms/listsort.html)

~

\Implementacion{Sort}{\Inout{lista}{lista(puntero(nodoLink))}, \In{fechas}{arreglo[3] de nat}}{}
\begin{algorithmic}
	\State var i, n, newn : nat
	\State var it : itLista(puntero(nodoLink))
	\State var p1, p2 : puntero(nodoLink)

	\State n \asignar Longitud(lista)
	\If{$n < 2$}
		\State n \asignar 0
	\EndIf

	\While{$n > 0$}
		\State i \asignar 0
		\State newn \asignar 0
		\State it \asignar CrearIt(lista)

		\State Avanzar(it)

		\While{HaySiguiente(it) $\land~ i < n$}
			\State p1 \asignar Anterior(it)
			\State p2 \asignar Siguiente(it)
			\If{CalcularAccesosRecientes((*p1).accesos, fechas) $>$~ CalcularAccesosRecientes((*p2).accesos, fechas)}
				\State EliminarSiguiente(it)
				\State EliminarAnterior(it)
				\State AgregarComoAnterior(it,p2)
				\State AgregarComoSiguiente(it,p1)
				\State newn \asignar i
			\EndIf
			\State i \asignar i + 1
			\State Avanzar(it)
		\EndWhile

		\State n \asignar newn
	\EndWhile
\end{algorithmic}

\end{Algoritmos}
